update-spec1(k;x;n;s,v.f(s;v)) == <k,x> : [<n,s,v. f(s;v)>] 

latex

---

clarification:

update-spec1(k;x;n;s,v.f(s;v)) == <k,x> : <n,s,v. f(s;v)>.nil 

latex

Definitions	x : v, car.cdr, <a,b>, x.A(x), nil
FDL editor aliases	update-spec1